@Article{HW:10:CSBMCCFP,
  author =       {Geng-Dian Huang and Bow-Yaw Wang},
  title =        {Complete {SAT}-Based Model Checking for Context-Free Processes},
  journal =      {International Journal of Foundations of Computer Science},
  year =         {2010},
  volume =    {21},
  number =    {2},
  pages =     {115-132},
}

@article{FinkelWW97,
  author    = {Alain Finkel and
               Bernard Willems and
               Pierre Wolper},
  title     = {A direct symbolic approach to model checking pushdown systems},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {9},
  year      = {1997},
  pages     = {27-37}
}

@inproceedings{EsparzaHRS00,
  author    = {Javier Esparza and
               David Hansel and
               Peter Rossmanith and
               Stefan Schwoon},
  title     = {Efficient Algorithms for Model Checking Pushdown Systems},
  booktitle = {CAV},
  year      = {2000},
  pages     = {232-247}
}

@inproceedings{EsparzaS01,
  author    = {Javier Esparza and
               Stefan Schwoon},
  title     = {A {BDD}-Based Model Checker for Recursive Programs},
  booktitle = {CAV},
  year      = {2001},
  pages     = {324-336}
}

@inproceedings{BallR00,
  author    = {Thomas Ball and
               Sriram K. Rajamani},
  title     = {Bebop: {A} Symbolic Model Checker for {B}oolean Programs},
  booktitle = {SPIN},
  year      = {2000},
  pages     = {113-130}
}

@inproceedings{AlurEY01,
  author    = {Rajeev Alur and
               Kousha Etessami and
               Mihalis Yannakakis},
  title     = {Analysis of Recursive State Machines},
  booktitle = {CAV},
  year      = {2001},
  pages     = {207-220}
}

@inproceedings{BaslerKW07_SPIN,
  author    = {G{\'e}rard Basler and
               Daniel Kroening and
               Georg Weissenbacher},
  title     = {{SAT}-Based Summarization for {B}oolean Programs},
  booktitle = {SPIN},
  year      = {2007},
  pages     = {131-148}
}

@inproceedings{BaslerKW07_HVC,
  author    = {G{\'e}rard Basler and
               Daniel Kroening and
               Georg Weissenbacher},
  title     = {A Complete Bounded Model Checking Algorithm for Pushdown
               Systems},
  booktitle = {Haifa Verification Conference},
  year      = {2007},
  pages     = {202-217}
}

@inproceedings{CookKS05,
  author    = {Byron Cook and
               Daniel Kroening and
               Natasha Sharygina},
  title     = {Symbolic Model Checking for Asynchronous {B}oolean Programs},
  booktitle = {SPIN},
  year      = {2005},
  pages     = {75-90}
}

@inproceedings{BiereCCZ99,
  author    = {Armin Biere and
               Alessandro Cimatti and
               Edmund M. Clarke and
               Yunshan Zhu},
  title     = {Symbolic Model Checking without {BDD}s},
  booktitle = {TACAS},
  year      = {1999},
  pages     = {193-207}
}

@inproceedings{SheeranSS00,
  author    = {Mary Sheeran and
               Satnam Singh and
               Gunnar St{\aa}lmarck},
  title     = {Checking Safety Properties Using Induction and a {SAT}-Solver},
  booktitle = {FMCAD},
  year      = {2000},
  pages     = {108-125}
}

@inproceedings{McMillan03,
  author    = {Kenneth L. McMillan},
  title     = {Interpolation and {SAT}-Based Model Checking},
  booktitle = {CAV},
  year      = {2003},
  pages     = {1-13}
}

@inproceedings{Bradley11,
  author    = {Aaron R. Bradley},
  title     = {{SAT}-Based Model Checking without Unrolling},
  booktitle = {VMCAI},
  year      = {2011},
  pages     = {70-87}
}

@inproceedings{SuwimonteerabuthES08,
  author    = {Dejvuth Suwimonteerabuth and
               Javier Esparza and
               Stefan Schwoon},
  title     = {Symbolic Context-Bounded Analysis of Multithreaded {J}ava
               Programs},
  booktitle = {SPIN},
  year      = {2008},
  pages     = {270-287}
}

@inproceedings{EsparzaKS06,
  author    = {Javier Esparza and
               Stefan Kiefer and
               Stefan Schwoon},
  title     = {Abstraction Refinement with {C}raig Interpolation and Symbolic
               Pushdown Systems},
  booktitle = {TACAS},
  year      = {2006},
  pages     = {489-503}
}

@inproceedings{BouajjaniEM97,
  author    = {Ahmed Bouajjani and
               Javier Esparza and
               Oded Maler},
  title     = {Reachability Analysis of Pushdown Automata: {A}pplication
               to Model-Checking},
  booktitle = {CONCUR},
  year      = {1997},
  pages     = {135-150}
}

@inproceedings{BallR02,
  author    = {Thomas Ball and
               Sriram K. Rajamani},
  title     = {The {SLAM} project: {D}ebugging system software via static analysis},
  booktitle = {POPL},
  year      = {2002},
  pages     = {1-3}
}

@inproceedings{QadeerR05,
  author    = {Shaz Qadeer and
               Jakob Rehof},
  title     = {Context-Bounded Model Checking of Concurrent Software},
  booktitle = {TACAS},
  year      = {2005},
  pages     = {93-107}
}

@inproceedings{BouajjaniFQ07,
  author    = {Ahmed Bouajjani and
               S{\'e}verine Fratani and
               Shaz Qadeer},
  title     = {Context-Bounded Analysis of Multithreaded Programs with
               Dynamic Linked Structures},
  booktitle = {CAV},
  year      = {2007},
  pages     = {207-220}
}

@inproceedings{AtigBQ09,
  author    = {Mohamed Faouzi Atig and
               Ahmed Bouajjani and
               Shaz Qadeer},
  title     = {Context-Bounded Analysis for Concurrent Programs with Dynamic
               Creation of Threads},
  booktitle = {TACAS},
  year      = {2009},
  pages     = {107-123}
}

@inproceedings{LalRB05,
  author    = {Akash Lal and
               Thomas W. Reps and
               Gogul Balakrishnan},
  title     = {Extended Weighted Pushdown Systems},
  booktitle = {CAV},
  year      = {2005},
  pages     = {434-448}
}

@inproceedings{LalR06,
  author    = {Akash Lal and
               Thomas W. Reps},
  title     = {Improving Pushdown System Model Checking},
  booktitle = {CAV},
  year      = {2006},
  pages     = {343-357}
}

@inproceedings{LalTKR08,
  author    = {Akash Lal and
               Tayssir Touili and
               Nicholas Kidd and
               Thomas W. Reps},
  title     = {Interprocedural Analysis of Concurrent Programs Under a
               Context Bound},
  booktitle = {TACAS},
  year      = {2008},
  pages     = {282-298}
}

@inproceedings{LalR08,
  author    = {Akash Lal and
               Thomas W. Reps},
  title     = {Reducing Concurrent Analysis Under a Context Bound to Sequential
               Analysis},
  booktitle = {CAV},
  year      = {2008},
  pages     = {37-51}
}

@article{Ramalingam00,
  author    = {G. Ramalingam},
  title     = {Context-sensitive synchronization-sensitive analysis is
               undecidable},
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {22},
  number    = {2},
  year      = {2000},
  pages     = {416-430}
}

@INPROCEEDINGS{pdr, 
author={Een, N. and Mishchenko, A. and Brayton, R.}, 
booktitle={FMCAD}, 
title={Efficient implementation of property directed reachability}, 
year={2011}, 
pages={125 -134},
}

@INPROCEEDINGS{ic3-2,
year={2012},
booktitle={CAV},
title={{IC3} and beyond: Incremental, Inductive Verification},
author={Bradley, AaronR.},
pages={4-4}
}


@inproceedings{BrummayerB09,
  author    = {Robert Brummayer and
               Armin Biere},
  title     = {Boolector: An Efficient {SMT} Solver for Bit-Vectors and Arrays},
  booktitle = {TACAS},
  year      = {2009},
  pages     = {174-177},
}
@inproceedings{rhs:popl:1995,
  author    = {Thomas W. Reps and Susan Horwitz and Shmuel Sagiv},
  title     = {Precise Interprocedural Dataflow Analysis via Graph Reachability},
  booktitle = {POPL},
  year      = {1995},
  pages     = {49-61}
}

@inproceedings{BraytonM10,
  author    = {Robert K. Brayton and
               Alan Mishchenko},
  title     = {{ABC}: {A}n Academic Industrial-Strength Verification Tool},
  booktitle = {CAV},
  year      = {2010},
  pages     = {24-40},
}

@inproceedings{EenMS07,
  author    = {Niklas E{\'e}n and
               Alan Mishchenko and
               Niklas S{\"o}rensson},
  title     = {Applying Logic Synthesis for Speeding Up {SAT}},
  booktitle = {SAT},
  year      = {2007},
  pages     = {272-286},
}
